Nuprl Lemma : w_locl_wf
11,40
postcript
pdf
w
:World,
a
,
b
:E. w_locl(
w
;
a
;
b
)
latex
Definitions
World
,
t
T
,
x
:
A
.
B
(
x
)
,
E
,
Type
,
w-pred(
w
;
e
)
,
x
.
A
(
x
)
,
P
Q
,
pred(
e
)
,
s
=
t
,
first(
e
)
,
b
,
A
,
A
c
B
,
x
:
A
B
(
x
)
,
R
^+
,
f
(
a
)
,
x
f
y
,
w_locl(
w
;
x
;
y
)
Lemmas
rel
plus
wf
,
not
wf
,
assert
wf
,
first
wf
,
pred
wf
,
w-pred
wf
,
w-E
wf
,
world
wf
origin
w:World, a, b:E. w_locl(w;a;b) 
w:World, a, b:E. w_locl(w;a;b) Tx:A. B(x)
x.A(x)
Q
b
A
B
B(x)